Search for: All records

Formally verifying system properties is one of the most effective ways of improving system quality, but its high manual effort requirements often render it prohibitively expensive. Tools that automate formal verification by learning from proof corpora to synthesize proofs have just begun to show their promise. These tools are effective because of the richness of the data the proof corpora contain. This richness comes from the stylistic conventions followed by communities of proof developers, together with the powerful logical systems beneath proof assistants. However, this richness remains underexploited, with most work thus far focusing on architecture rather than on how to make the most of the proof data. This article systematically explores how to most effectively exploit one aspect of that proof data: identifiers. We develop the Passport approach, a method for enriching the predictive Coq model used by an existing proof-synthesis tool with three new encoding mechanisms for identifiers: category vocabulary indexing, subword sequence modeling, and path elaboration. We evaluate our approach’s enrichment effect on three existing base tools: ASTactic, Tac, and Tok. In head-to-head comparisons, Passport automatically proves 29% more theorems than the best-performing of these base tools. Combining the three tools enhanced by the Passport approach automatically proves 38% more theorems than combining the three base tools. Finally, together, these base tools and their enhanced versions prove 45% more theorems than the combined base tools. Overall, our findings suggest that modeling identifiers can play a significant role in improving proof synthesis, leading to higher-quality software. 

Formally verified correctness is one of the most desirable properties of software systems. But despite great progress made via interactive theorem provers, such as Coq, writing proof scripts for verification remains one of the most effort-intensive (and often prohibitively difficult) software development activities. Recent work has created tools that automatically synthesize proofs or proof scripts. For example, CoqHammer can prove 26.6% of theorems completely automatically by reasoning using precomputed facts, while TacTok and ASTactic, which use machine learning to model proof scripts and then perform biased search through the proof-script space, can prove 12.9% and 12.3% of the theorems, respectively. Further, these three tools are highly complementary; together, they can prove 30.4% of the theorems fully automatically. Our key insight is that control over the learning process can produce a diverse set of models, and that, due to the unique nature of proof synthesis (the existence of the theorem prover, an oracle that infallibly judges a proof's correctness), this diversity can significantly improve these tools' proving power. Accordingly, we develop Diva, which uses a diverse set of models with TacTok's and ASTactic's search mechanism to prove 21.7% of the theorems. That is, Diva proves 68% more theorems than TacTok and 77% more than ASTactic. Complementary to CoqHammer, Diva proves 781 theorems (27% added value) that Coq-Hammer does not, and 364 theorems no existing tool has proved automatically. Together with CoqHammer, Diva proves 33.8% of the theorems, the largest fraction to date. We explore nine dimensions for learning diverse models, and identify which dimensions lead to the most useful diversity. Further, we develop an optimization to speed up Diva's execution by 40X. Our study introduces a completely new idea for using diversity in machine learning to improve the power of state-of-the-art proof-script synthesis techniques, and empirically demonstrates that the improvement is significant on a dataset of 68K theorems from 122 open-source software projects. 

Abstract Volcán Quizapu, Chile, is an under-monitored volcano that was the site of two historical eruptions: an effusive eruption in 1846–1847 and a Plinian eruption in 1932, both of which discharged ∼5 km3 (dense rock equivalent) of lava and/or tephra. The majority of material erupted in both cases is trachydacite, nearly identical for each event. We present H2O-saturated, phase equilibrium experiments on this end-member dacite magma, using a pumice sample from the 1932 eruption as the main starting material. At an oxygen fugacity (fO2) of ∼NNO + 0·2 (where NNO is the nickel–nickel oxide buffer), the phase assemblage of An25–30 plagioclase + amphibole + orthopyroxene, without biotite, is stable at 865 ± 10 °C and 110 ± 20 MPa H2O pressure (PH2O), corresponding to ∼4 km depth. At these conditions, experiments also reproduce the quenched glass composition of the starting pumice. At slightly higher PH2O and below 860 °C, biotite joins the equilibrium assemblage. Because biotite is not part of the observed Quizapu phase assemblage, its presence places an upper limit on PH2O. At the determined storage PH2O of ∼110 MPa, H2O undersaturation of the magma with XH2Ofluid = 0·87 would align Ptotal to mineral-based geobarometry estimates of ∼130 MPa. However, XH2Ofluid < 1 is not required to reproduce the Quizapu dacite phase assemblage and compositions. A second suite of experiments at lower fO2 shows that the stability fields of the hydrous silicates (amphibole and biotite) are significantly restricted at NNO – 2 relative to NNO + 0·2. Additional observations of Quizapu lava and pumice samples support the existing hypothesis that rapid pre-eruptive heating drove the effusive 1846–1847 eruption, with important refinements. We demonstrate that microlites in the end-member dacite lavas are consistent with in situ crystallization (during ascent), rather than transfer from an andesite. In one end-member dacite lava, newly identified reverse zoning in orthopyroxene and incipient destabilization of amphibole are consistent with small degrees of heating. Our work articulates a clear direction for future Quizapu studies, which are warranted given the active nature of the Cerro Azul–Descabezado Grande volcanic axis.